perm filename PERMF[EKL,SYS]1 blob
sn#818132 filedate 1986-06-05 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00028 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00004 00002 functions as lists of numbers
C00005 00003 definitions of composition,identity, inverse as functions
C00008 00004 a list of elementary facts
C00013 00005 a list of the theorems and lemmata proved
C00017 00006 *-- proofs: condition for def_appl
C00018 00007
C00021 00008 lemma sortcomp
C00022 00009 sorts of the other functions
C00023 00010 lemma length_compose
C00028 00011 lemmata nth_compose, nthcdr_compose
C00031 00012 perm compose to finish ***to finish***
C00037 00013 length ident and lengthinverse
C00044 00014 improved version
C00047 00015 theorem 1: associativity of compose
C00050 00016 identity right
C00052 00017 identity right ***try again***
C00055 00018 an attempt to make this proof shorter ***try again***
C00057 00019 id main ***try again***
C00060 00020 a more compact version of the proof id main
C00063 00021 perm ident
C00064 00022 identity left
C00065 00023 inv main ***try again***
C00069 00024 a more compact version of the proof inv main
C00072 00025 perm inverse: part 1 (into inverse)
C00075 00026 perm inverse: part 2 (onto inverse)
C00080 00027 compose_inverse_right
C00085 00028 compose inverse left ***try again***
C00090 ENDMK
C⊗;
;functions as lists of numbers
(wipe-out)
(get-proofs appl prf prm glb)
;definitions of composition,identity, inverse as functions
(proof comp_fnct)
;the condition for λx.appl(v,x) to be defined on u as domain is that u satisfies
;allp(λx.natnum(x)∧x<length(v),u)
(decl def_appl (type: |@u⊗@u→truthval|))
(define def_appl |∀u v.def_appl(v,u)≡allp(λx.natnum(x)∧x<length(v),u)|)
(label def_appl_fact)
;composition of functions
(decl (compose) (infixname: |⊗|) (type: |ground⊗ground→ground|) (syntype: constant)
(bindingpower: 930))
(define compose |∀u v x.(u⊗nil)=nil∧
(u⊗(x.v))=(nth(u,x)).(u⊗v)|listinductiondef)
(label composedef)
;the identity function
(decl (ident1) (type: |ground⊗ground→ground|))
(defax ident1 |∀x u n i.ident1(i,0)=nil∧
ident1(i,n')=i.ident1(i',n)|)
(label identdef1)
(decl (ident) (type: |ground→ground|))
(define ident |∀n.ident(n)=ident1(0,n)|)
(label identdef)
;the inverse of a function
(decl (invers1) (type: |ground⊗ground⊗ground→ground|))
(defax invers1 |∀u i n.invers1(u,i,0)=nil∧invers1(nil,i,n)=nil∧
invers1(u,i,n')=if null(fstposition(u,i)) then nil
else fstposition(u,i).invers1(u,i',n)|)
(label inversdef1)
(decl (inverse) (type: |ground→ground|))
(define inverse|∀u.inverse(u)=invers1(u,0,length(u))|)
(label inversdef)
;a list of elementary facts
(proof permfacts)
;a condition for def_appl
(axiom |∀u v.into(u)∧length(u)≤length(v)⊃def_appl(v,u)|)
(label def_appl_condition)
;facts about sorts
;compose
(axiom |∀V U.DEF_APPL(V,U)⊃LISTP V⊗U|)
(label sortcomp)(label simpinfo)
(axiom |∀V U.ALLP(λX.NATNUM(X)∧X<LENGTH V,U)⊃LISTP V⊗U|)
(label simpinfo)
;ident
(axiom |∀m n.listp ident1(m,n)|)
(label simpinfo)
(axiom |∀n.listp ident(n)|)
(label simpinfo)
;inverse
(axiom |∀u n i.listp invers1(u,i,n)|)
(label simpinfo)
(axiom |∀u.listp inverse(u)|)
(label simpinfo)
;facts about the length
;lemma length_compose
(axiom |∀w u.def_appl(w,u)⊃length(w⊗u)=length(u)|)
(label length_compose)
;identity_length
(axiom |∀N M.LENGTH (IDENT1(M,N))=N|)
(label ident_length) (label simpinfo)
(axiom |∀N.LENGTH (IDENT(N))=N|)
(label simpinfo)
;inverse length
(axiom |∀u.perm u⊃length inverse(u)=length u|)
(label lengthinverse)
;a list of the theorems and lemmata proved
(proof permf)
; (axiom |∀u.into(u)≡allp(λx.(natnum x∧x<length u),u)|)
; (label intofact)
;compose
;lemma nth_compose
(axiom |∀V U N.DEF_APPL(V,U)∧N<LENGTH U⊃NTH(V⊗U,N)=NTH(V,NTH(U,N))|)
(label nth_compose)
;lemma nthcdr_compose
(axiom |∀V U N.DEF_APPL(V,U)⊃NTHCDR(V⊗U,N)=V⊗NTHCDR(U,N)|)
(label nthcdr_compose)
;theorem 1
(axiom |∀W V U.DEF_APPL(W,V)∧DEF_APPL(V,U)⊃(W⊗V)⊗U=W⊗(V⊗U)|)
(label assoc_comp)
;lemma perm_compose
(axiom |∀u v.perm(u)∧perm(v)∧length(u)=length(v)⊃perm(u⊗v)|)
(label perm_compose)
;ident
;theorem 2(i)
(axiom |∀U.U⊗IDENT(LENGTH U)=U|)
(label identity_right_theorem)
;we prove it using the following lemma
;∀N.N≤LENGTH U⊃U⊗IDENT1(LENGTH U-N,N)=NTHCDR(U,LENGTH U-N)
;lemma id_main
(axiom |∀M N.N<M⊃NTH(IDENT(M),N)=N|)
(label id_main)
;we prove it using the following fact
(axiom |∀M N.N<M⊃NTHCDR(IDENT(M),N)=IDENT1(N,M-N)|)
(label id_main_part2)
;lemma perm_ident
(axiom |∀n.perm(ident n)|)
(label perm_id)
;theorem 2(ii)
(axiom |∀U.INTO(U)⊃IDENT(LENGTH U)⊗U=U|)
(label identity_left_theorem)
;inverse
;lemma nth_fstposition
(axiom |∀u n.member(n,u)⊃nth(u,fstposition(u,n))=n|)
(label nth_fstposition)
;for a proof of this see the file permp[prm,glb]
;lemma fstposition_nth
(axiom |∀U N.UNIQUENESS(U)∧N<LENGTH U⊃FSTPOSITION(U,NTH(U,N))=N|)
(label fstposition_nth)
;for a proof of this see the file nth1[prm,glb]
;the pigeon-hole principle
(axiom |∀u.perm(u)⊃inj(u)|)
(label perm_injectivity)
;(For a proof of this see the the file nth1[prm,glb]
;lemma inv_main
(axiom |∀U N.PERM U∧N<LENGTH(U)⊃NTH(INVERSE(U),N)=FSTPOSITION(U,N)|)
(label inv_main)
;we prove this using the following fact
(axiom |∀U N.PERM U∧N<LENGTH U⊃NTHCDR(INVERSE(U),N)=INVERS1(U,N,LENGTH U-N)|)
(label inv_main_part2)
;lemma perm inverse
(axiom |PERM(U)⊃PERM(INVERSE U)|)
(label perm_inverse)
;theorem 3
(axiom |∀U.PERM(U)⊃U⊗INVERSE U=IDENT(LENGTH U)|)
(label compose_inverse_right)
(axiom |∀U.PERM(U)⊃INVERSE U⊗U=IDENT(LENGTH U)|)
(label compose_inverse_left)
;*-- proofs: condition for def_appl
(assume |into u|)
(assume |length u≤length v|)
(rw -2 (open into))
;∀N.N<LENGTH U⊃NATNUM(NTH(U,N))∧NTH(U,N)<LENGTH U
(trw |∀n.n<length u⊃natnum nth(u,n)∧nth(u,n)<length v| * (less_lesseq_fact1 -2))
;∀N.N<LENGTH U⊃NATNUM(NTH(U,N))∧NTH(U,N)<LENGTH V
(ue ((phi1.|λx.natnum x∧x<length v|)(u.u)) nth_allp *)
;ALLP(λX.NATNUM(X)∧X<LENGTH V,U)
(trw |def_appl(v,u)| (open def_appl) *)
;DEF_APPL(V,U)
(ci (-6 -5))
;INTO(U)∧LENGTH U≤LENGTH V⊃DEF_APPL(V,U)
(label def_appl_condition)
;
(rw def_appl_condition (open lesseq) (use normal mode: always))
;∀U V.(INTO(U)∧LENGTH U=LENGTH V⊃DEF_APPL(V,U))∧
; (INTO(U)∧LENGTH U<LENGTH V⊃DEF_APPL(V,U))
(derive |perm u∧length u = length v⊃def_appl(v,u)|
(def_appl_condition *)(open perm onto))
;lemma sortcomp
(unlabel simpinfo sortcomp)
(ue (phi |λu.def_appl(v,u)⊃listp v⊗u|) listinduction
(part 1 (open def_appl allp compose )))
;∀U.DEF_APPL(V,U)⊃LISTP V⊗U
(label simpinfo sortcomp)
;sorts of the other functions
(unlabel simpinfo permf#9)
(ue (a |λn.∀m.listp ident1(m,n)|) proof_by_induction (open ident1))
;∀N M.LISTP IDENT1(M,N)
(trw |∀n.listp ident(n)| (open ident) *)
;∀N.LISTP IDENT(N)
(ue (a |λn.∀i.listp invers1(u,i,n)|) proof_by_induction (open invers1) posfacts)
;∀N I.LISTP INVERS1(U,I,N)
(trw |listp inverse(u)| (open inverse) *)
;LISTP INVERSE(U)
;lemma length_compose
(proof length_compose)
(assume |def_appl(w,u)|)
(label l_c_1)
(rw * (open def_appl))
(label l_c_2)
;ALLP(λX.NATNUM(X)∧X<LENGTH W,U)
(assume |n<length(u)|))
(label l_c_3)
(ue ((u.u)(x.|nth(u,n)|)(phi1.|λx.natnum(x)∧x<length(w)|)) allp_elimination
nthmember sexp_nth l_c_3 l_c_2)
;NATNUM(NTH(U,N))∧NTH(U,N)<LENGTH W
(label l_c_4)
(trw |sexp(nth(w,nth(u,n)))| sexp_nth l_c_4)
;SEXP NTH(W,NTH(U,N))
(label l_c_sort1)
(ci l_c_3)
;N<LENGTH U⊃SEXP NTH(W,NTH(U,N))
(label l_c_7)
(derive |allp(λX.NATNUM(X)∧X<LENGTH W,NTHCDR(U,N'))| (allp_nthcdr l_c_2))
;ALLP(λX.NATNUM(X)∧X<LENGTH W,NTHCDR(U,N'))
(derive |listp(w⊗nthcdr(u,n'))| (* sortcomp))
(label l_c_sort2)
(ci l_c_3)
;N<LENGTH U⊃LISTP W⊗NTHCDR(U,N')
(label l_c_8)
(ue ((phi.|λu.length(w⊗u)=length(u)|)(u.u)) nthcdr_induction
(part 1(open compose length )) l_c_7 l_c_8)
;LENGTH (W⊗U)=LENGTH U
(ci L_C_1)
;DEF_APPL(W,U)⊃LENGTH (W⊗U)=LENGTH U
;LEMMA
;DEF_APPL(W,U)⊃LENGTH (W⊗U)=LENGTH U
;Proof: by nthcdr_induction applied to U. For U = NIL, the result is given by the
;definition of compose. Assume LENGTH(W⊗NTHCDR(U,N'))=LENGTH(NTHCDR(U,N')), for N'
;less than LENGTH(U); want
;LENGTH(W⊗(NTH(U,N).NTHCDR(U,N'))=LENGTH(NTH(U,N).NTHCDR(U,N'))
;Since N is less than LENGTH(U), NTH(U,N) is an s-expression, so we can apply the
;definition of compose; the left hand side is
;LENGTH(NTH(W,NTH(U,N)).(W⊗NTHCDR(U,N')))
;so the inductive step will be proved if we show that, under the given assumption
;[line l_c_1], the terms are of the proper sorts. This is done as follows:
;Since W is defined as an application on U as domain [line l_c_1], NTH(U,N) is a
;natural number less than LENGTH(W). Therefore NTH(W,NTH(U,N)) is an s-expression
;[line l_c_sort1]. On the other hand, W is defined as an application on any part
;of U, since it is defined on U (using ALLP_NTHCDR) therefore W⊗NTHCDR(U,N') is
;a defined and is a list (using SORTCOMP).
;facts used:
;labels: LESS_LESSEQ_FACT1 (proof minus)
;∀N M K.N<M∧M≤K⊃N<K
;labels: SIMPINFO SEXP_NTH
;(AXIOM |∀U N.N<LENGTH U⊃SEXP NTH(U,N)|)
;labels: NTHMEMBER
;(AXIOM |∀U N.N<LENGTH U⊃MEMBER(NTH(U,N),U)|)
;labels: allp_elimination
;∀U.MEMBER(X,U)∧ALLP(PHI1,U)⊃PHI1(X)
;labels: ALLP_NTHCDR
;∀U N.ALLP(A,U)⊃ALLP(A,NTHCDR(U,N))
;labels: SIMPINFO SORTCOMP
;∀U.ALLP(λX.NATNUM(X)∧X<LENGTH V,U)⊃LISTP V⊗U
;labels: NTHCDR_INDUCTION
;(AXIOM |∀PHI U.PHI(NIL)∧
(∀N.N<LENGTH U⊃(PHI(NTHCDR(U,N'))⊃PHI(NTH(U,N).NTHCDR(U,N'))))⊃ PHI(U)|)
(show *)
;lemmata nth_compose, nthcdr_compose
(proof nth_compose)
;lemma nthcompose
;by double induction on n and u
;labels: DOUBLEINDUCTION1
;(∀U N X.PHI3(NIL,N)∧PHI3(U,0)∧(PHI3(U,N)⊃PHI3(X.U,N')))⊃(∀U N.PHI3(U,N))
;one base_case is proved by listinduction
(ue (phi |λu.¬null(u)∧def_appl(v,u)⊃nth(v⊗u,0)=nth(v,nth(u,0))|) listinduction
(part 1(open compose nth def_appl allp)) )
;∀U.¬NULL U∧DEF_APPL(V,U)⊃CAR (V⊗U)=NTH(V,CAR U)
(label a_c_base1)
;and the other is trivial; so
(ue (phi3 |λu n.def_appl(v,u)∧n<length(u)⊃nth(v⊗u,n)=nth(v,nth(u,n))|) doubleinduction1
(part 1(open compose def_appl allp)) a_c_base1)
;∀U N.DEF_APPL(V,U)∧N<LENGTH U⊃NTH(V⊗U,N)=NTH(V,NTH(U,N))
(label nth_compose)
; the similar fact for nthcdr is also easy
;nthcdr_compose
(ue (phi3 |λu n.n<length(u)∧def_appl(v,u)⊃nthcdr(v⊗u,n)=v⊗nthcdr(u,n)|) doubleinduction1
(part 1(open compose nthcdr def_appl allp)))
;∀U N.N<LENGTH U∧DEF_APPL(V,U)⊃NTHCDR(V⊗U,N)=V⊗NTHCDR(U,N)
(label nthcdr_comp1)
(trw |∀u v n.length(u)≤n∧def_appl(v,u)⊃length(v⊗u)≤n| length_compose)
(trw |∀u n.length(u)≤n∧def_appl(v,u)⊃nthcdr(v⊗u,n)=v⊗nthcdr(u,n)| *
(use trivial_nthcdr mode: always) (open compose))
;∀U N.LENGTH U≤N∧DEF_APPL(V,U)⊃NTHCDR(V⊗U,N)=V⊗NTHCDR(U,N)
(label nthcdr_comp2)
(derive |(p⊃r)∧(q⊃r)∧(p∨q)⊃r|)
(ue ((p.|length u≤n|)(q.|n<length u|)(r.|def_appl(v,u)⊃nthcdr(v⊗u,n)=v⊗nthcdr(u,n)|))
* nthcdr_comp2 nthcdr_comp1 trichotomy2)
;DEF_APPL(V,U)⊃NTHCDR(V⊗U,N)=V⊗NTHCDR(U,N)
;perm compose; to finish ***to finish***
(proof perm_compose)
1. (assume |perm u|)
(label pc1)
2. (assume |perm v|)
(label pc2)
3. (assume |length u = length v|)
(label pc3)
4. (rw pc2 (open perm onto))
(label pc4)
;INTO(V)∧(∀N.N<LENGTH V⊃MEMBER(N,V))
;deps: (PC2)
5. (ue ((u.v)(v.u)) def_appl_condition (open lesseq) pc3 pc4)
;DEF_APPL(U,V)
(label pc5)
;deps: (PC2 PC3)
6. (ue ((u.v)(w.u)) length_compose pc5)
;LENGTH (U⊗V)=LENGTH V
(label pc6)
;deps: (PC2 PC3)
7. (assume |n<length(u⊗v)|)
(label pc7)
8. (rw * (use pc6 mode: exact))
;N<LENGTH V
(label pc8)
;deps: (PC2 PC3 PC7)
9. (rw pc2 (open perm onto into))
;(∀N.N<LENGTH V⊃NATNUM(NTH(V,N))∧NTH(V,N)<LENGTH V)∧
;(∀N.N<LENGTH V⊃MEMBER(N,V))
(label pc9)
;deps: (PC2)
10. (derive |natnum(nth(v,n))∧nth(v,n)<length u| (pc8 *)
(use pc3 mode: exact))
(label pc10)
;deps: (PC2 PC3 PC7)
11. (rw pc1 (open perm onto into))
;(∀N.N<LENGTH U⊃NATNUM(NTH(U,N))∧NTH(U,N)<LENGTH U)∧
;(∀N.N<LENGTH U⊃MEMBER(N,U))
(label pc11)
;deps: (PC1)
12. (ue (n |nth(v,n)|) * pc10)
;NATNUM(NTH(U,NTH(V,N)))∧NTH(U,NTH(V,N))<LENGTH U∧MEMBER(NTH(V,N),U)
(label pc12)
;deps: (PC1 PC2 PC3 PC7)
13. (derive |nth(u⊗v,n)=nth(u,nth(v,n))| (nth_compose pc5 pc8))
(label pc13)
;deps: (PC2 PC3 PC7)
14. (trw |natnum nth(u⊗v,n)∧nth(u⊗v,n)<length(u⊗v)| pc12
(use pc13 pc6 mode: exact)
(use pc3 mode: exact direction: reverse))
;NATNUM(NTH(U⊗V,N))∧NTH(U⊗V,N)<LENGTH (U⊗V)
;deps: (PC1 PC2 PC3 PC7)
15. (ci pc7)
;N<LENGTH (U⊗V)⊃NATNUM(NTH(U⊗V,N))∧NTH(U⊗V,N)<LENGTH (U⊗V)
;deps: (PC1 PC2 PC3)
16. (trw |into(u⊗v)| * (open into) pc5)
;INTO(U⊗V)
(label pc_into)
;deps: (PC1 PC2 PC3)
;part 2
17. (rw pc8 (use pc3 mode: exact direction: reverse))
;N<LENGTH U
(label pc20)
;deps: (PC2 PC3 PC7)
;labels: MEMBER_NTH
;∀U Y.MEMBER(Y,U)⊃(∃N.N<LENGTH U∧NTH(U,N)=Y)
18. (define jv |jv<length u ∧ nth(u,jv)=n| (* pc11 member_nth))
(label pc21)
;JV is unknown.
;the symbol JV is given the same declaration as J
;deps: (PC1 PC2 PC3 PC7)
19. (derive |jv<length v| * (use pc3 mode: exact direction: reverse))
;deps: (PC1 PC2 PC3 PC7)
20. (define kv |kv<length v ∧ nth(v,kv)=jv| (* pc9 member_nth))
(label pc22)
;KV is unknown.
;the symbol KV is given the same declaration as K
;deps: (PC1 PC2 PC3 PC7)
;labels: NTH_COMPOSE
;∀V U N.DEF_APPL(V,U)∧N<LENGTH U⊃NTH(V⊗U,N)=NTH(V,NTH(U,N))
21. (ue ((v.u)(u.v)(n.kv)) nth_compose pc5
(use * mode: always)(use pc21 mode: always))
(label pc23)
;NTH(U⊗V,KV)=N
;deps: (PC1 PC2 PC3 PC7)
22. (derive |kv<length(u⊗v)| (pc22 pc6))
;deps: (PC1 PC2 PC3 PC7)
;labels: NTHMEMBER
;∀U N.N<LENGTH U⊃MEMBER(NTH(U,N),U)
23. (trw |member(nth(u⊗v,kv),u⊗v)| (nthmember pc5 *))
;MEMBER(NTH(U⊗V,KV),U⊗V)
;deps: (PC1 PC2 PC3 PC7)
24. (rw * pc23)
;MEMBER(N,U⊗V)
;deps: (PC1 PC2 PC3 PC7)
25. (ci pc7)
;N<LENGTH (U⊗V)⊃MEMBER(N,U⊗V)
;deps: (PC1 PC2 PC3)
(label pc_onto)
26. (trw |perm(u⊗v)| (pc5 pc_into pc_onto) (open perm onto))
;PERM(U⊗V)
;deps: (PC1 PC2 PC3)
27. (ci (pc1 pc2 pc3))
;PERM(U)∧PERM(V)∧LENGTH U=LENGTH V⊃PERM(U⊗V)
(label perm_compose)
;length ident and lengthinverse
(ue (a |λn.∀m.length ident1(m,n)=n|) proof_by_induction (open ident1))
;∀N M.LENGTH (IDENT1(M,N))=N
;lemma lengthinverse
(proof lengthinverse)
(assume |perm u|)(label li1)
(rw * (open perm onto into))
;(∀N.N<LENGTH U⊃NATNUM(NTH(U,N))∧NTH(U,N)<LENGTH U)∧(∀N.N<LENGTH U⊃MEMBER(N,U))
(label li2)
(ue ((u.u)(y.n)) posfacts)
;(NULL FSTPOSITION(U,N)⊃¬MEMBER(N,U))∧(MEMBER(N,U)⊃NATNUM(FSTPOSITION(U,N)))
(derive |n<length u⊃¬null fstposition(u,n)| (* li2))
(label li3)
(ue (a |λn.n<length u⊃length invers1(u,length u-n,n)=n|) proof_by_induction
(open invers1)
(use * ue: ((n.|length u-n'|)) mode: always)
(use succ_less_less mode: exact)
(use minusfact10 ue: ((n.n)(m.|length u|)) mode: always direction: reverse)
(use minusfact11 ue: ((m.n)(n.|length u|)) mode: always))
;∀N.N<LENGTH U⊃LENGTH (INVERS1(U,LENGTH U-N,N))=N
(label li_lemma)
;with the help of this lemma the result follows easily by cases
(trw |null u⊃length inverse(u)=length u| (open inverse invers1))
;NULL U⊃LENGTH (INVERSE(U))=LENGTH U
(label li4)
(assume |¬null u|)
(label li5)
(ue (n |length u|) zeroleast (open lesseq) *)
;0<LENGTH U
(label li6)
(ue (n |length u|) minusfact5 *)
;PRED(LENGTH U)'=LENGTH U
(label li7)
(trw |pred(length u)<length u| (use li7 mode: exact direction: reverse) successor1)
;PRED(LENGTH U)<LENGTH U
(ue (n |pred(length u)|) li_lemma
* (use minus1 li6 mode: exact))
;LENGTH (INVERS1(U,1,PRED(LENGTH U)))=PRED(LENGTH U)
(label li8)
(trw |length inverse(u)| (open inverse invers1)
(use li7 mode: exact direction: reverse)
(use li3 li6 li8 mode: exact))
;LENGTH (INVERSE(U))=PRED(LENGTH U)'
(label li9)
(rw * (use minusfact5 li6 mode: exact))
;LENGTH (INVERSE(U))=LENGTH U
;deps: (LI1 LI5)
(ci li5)
;¬NULL U⊃LENGTH (INVERSE(U))=LENGTH U
(label li10)
(ue ((p.|length inverse(u)=length u|)(q.|null u|)) excluded_middle li4 li10)
;LENGTH (INVERSE(U))=LENGTH U
;deps: (LI1)
(ci li1)
;PERM(U)⊃LENGTH (INVERSE(U))=LENGTH U
;labels: MINUSFACT10
; (AXIOM |∀N M.N<M⊃M-N=(M-N')'|)
;labels: MINUSFACT11
; (AXIOM |∀N M.N<M⊃M-N'<M|)
;labels: MINUSFACT5
; (AXIOM |∀N.0<N⊃PRED(N)'=N|)
;improved version
1. (assume |perm(u)|)
(label li1)
2. (rw li1 (open perm onto into))
;(∀N.N<LENGTH U⊃NATNUM(NTH(U,N))∧NTH(U,N)<LENGTH U)∧(∀N.N<LENGTH U⊃MEMBER(N,U))
(label li2)
3. (ue ((u.|u|) (y.|n|)) posfacts)
;(NULL FSTPOSITION(U,N)⊃¬MEMBER(N,U))∧(MEMBER(N,U)⊃NATNUM(FSTPOSITION(U,N)))
4. (derive |n<length u⊃¬null fstposition(u,n)| (3 li2))
(label li3)
5. (ue ((m.|n|) (n.|length u|)) minusfact11
((part 1 (use less_lesseqsucc mode: exact))))
;N'≤LENGTH U⊃LENGTH U-N'<LENGTH U
6. (derive |n'≤length u⊃¬null fstposition(u,length u-n')| (5 li3))
(label li4)
7. (trw |n'≤length u⊃(length u-n')'=length u-n|
((use minusfact10)
(use less_lesseqsucc mode: exact direction: reverse)))
;N'≤LENGTH U⊃(LENGTH U-N')'=LENGTH U-N
8. (ue ((a.|λn.n≤length u⊃length (invers1(u,length u-n,n))=n|))
proof_by_induction
((open invers1) (use succ_lesseq_lesseq) (use 7) (use li4)))
;∀N.N≤LENGTH U⊃LENGTH (INVERS1(U,LENGTH U-N,N))=N
9. (ue (n |length u|) * (open lesseq))
;LENGTH (INVERS1(U,0,LENGTH U))=LENGTH U
10. (trw |length inverse(u)=length u| (open inverse) *)
;LENGTH (INVERSE(U))=LENGTH U
;deps: (LI1)
11. (ci li1)
;PERM(U)⊃LENGTH (INVERSE(U))=LENGTH U
;theorem 1: associativity of compose
(proof assoc_compose)
;associativity of compose
;by listinduction on u
(trw |def_appl(w,v)∧def_appl(v,u)⊃(w⊗v)⊗nil=w⊗(v⊗nil)|
(open compose ) sortcomp)
(label ass_comp_base)
(ue (phi |λu.def_appl(w,v)∧def_appl(v,u)⊃(w⊗v)⊗u=w⊗(v⊗u)|) listinduction
(part 1#2(open compose def_appl allp)) sortcomp ass_comp_base
(use nth_compose ue: ((v.w)(u.v)) ) )
;∀U.DEF_APPL(W,V)∧DEF_APPL(V,U)⊃(W⊗V)⊗U=W⊗(V⊗U)
(label assoc_comp)
;the conditions def_appl are satisfied
;if U and V are permutations of the same length
(assume |perm(v)∧perm(u)∧length(v)=length(u)∧length(w)=length(v)|)
(rw * (open perm onto))
;INTO(V)∧(∀N.N<LENGTH U⊃MEMBER(N,V))∧INTO(U)∧(∀N.N<LENGTH U⊃MEMBER(N,U))∧
;LENGTH V=LENGTH U∧LENGTH W=LENGTH U
(ue ((u.v)(v.w)) def_appl_condition * (open lesseq))
;DEF_APPL(W,V)
(ue ((u.u)(v.v)) def_appl_condition -2 (open lesseq))
;DEF_APPL(V,U)
(derive |(w⊗v)⊗u=w⊗(v⊗u)|(assoc_comp * -2))
(ci -5)
;PERM(V)∧PERM(U)∧LENGTH V=LENGTH U∧LENGTH W=LENGTH U⊃(W⊗V)⊗U=W⊗(V⊗U)
;identity right
(proof identity)
(rw perm_id (open perm onto))
;∀N.INTO(IDENT(N))∧(∀N1.N1<N⊃MEMBER(N1,IDENT(N)))
;labels: DEF_APPL_CONDITION
;∀U V.INTO(U)∧LENGTH U≤LENGTH V⊃DEF_APPL(V,U)
(ue ((u.|ident(length u)|)(v.u))
def_appl_condition * (open lesseq))
;DEF_APPL(U,IDENT(LENGTH U))
;labels: NTH_COMPOSE
1. (AXIOM |∀V U N.DEF_APPL(V,U)∧N<LENGTH U⊃NTH(V⊗U,N)=NTH(V,NTH(U,N))|)
(ue ((u.|ident(length u)|)(v.u)(n.n)) nth_compose *
(use id_main mode: exact))
;N<LENGTH U⊃NTH(U⊗IDENT(LENGTH U),N)=NTH(U,N)
;labels: EXTENSIONALITY
;∀U V.LENGTH U=LENGTH V∧(∀I.I<LENGTH U⊃APPL(U,I)=APPL(V,I))⊃U=V
(ue ((u.|u⊗ident(length u)|)(v.u)) extensionality (open appl)
(use length_compose -2 *))
;U⊗IDENT(LENGTH U)=U
;identity right ***try again***
(proof identity_right)
(ue ((u.u)(n.|length u|)) trivial_nthcdr (open lesseq))
;NTHCDR(U,LENGTH U)=NIL
(trw |u⊗ident1(length u,0)=NTHCDR(u,length u)| (open ident1 compose)
(use * mode: exact))
;U⊗IDENT1(LENGTH U,0)=NTHCDR(U,LENGTH U)
(label ir1)
(assume |n≤length(u)⊃u⊗ident1(length u-n,n)=nthcdr(u,length u-n)|)
(label ir_hyp)
(assume |n'≤length u|)(label ir2)
(derive |u⊗ident1(length u-n,n)=nthcdr(u,length u-n)| (ir_hyp ir2 succ_lesseq_lesseq))
(label ir3)
(derive |length u-(n')<length u| (minusfact11 less_lesseqsucc ir2))
(label ir4)
(derive |(length u-n')'=length u-n| (minusfact10 less_lesseqsucc ir2))
(label ir5)
(trw |u⊗ident1(length u-(n'),n')=nthcdr(u,length u-(n'))| (open ident1 compose)
(use nthcdr_car_cdr ue: ((u.u)(n.|length u-(n')|)) mode: exact) ir4 ir5 ir3)
;U⊗IDENT1(LENGTH U-N',N')=NTHCDR(U,LENGTH U-N')
;deps: (IR_HYP IR2)
(ci ir2)
;N'≤LENGTH U⊃U⊗IDENT1(LENGTH U-N',N')=NTHCDR(U,LENGTH U-N')
(ci ir_hyp)
(ue (a |λn.n≤length(u)⊃u⊗ident1(length u-n,n)=nthcdr(u,length u-n)|) proof_by_induction
(part 1#1(open minus)) ir1 *)
;∀N.N≤LENGTH U⊃U⊗IDENT1(LENGTH U-N,N)=NTHCDR(U,LENGTH U-N)
;the theorem follows immediately
(ue (n |length u|) * (open lesseq nthcdr) (use n_less_n))
;U⊗IDENT1(0,LENGTH U)=U
(trw |u⊗ident(length u)=u| (open ident) *)
;U⊗IDENT(LENGTH U)=U
;an attempt to make this proof shorter ***try again***
(proof identity_right)
(ue (a |λn.n≤length(u)⊃u⊗ident1(length u-n,n)=nthcdr(u,length u-n)|)
proof_by_induction (open ident1 compose)
(part 1#2#1 (use succ_lesseq_lesseq mode: exact))
(part 1#2#1#1 (use minusfact10 less_lesseqsucc mode: exact)
(use nthcdr_car_cdr
ue: ((u.u)(n.|length(u)-n'|)) minusfact11 mode: exact))
(part 1#1(use trivial_nthcdr)))
;(0≤LENGTH U⊃NIL=NTHCDR(U,LENGTH U-0))∧
;(∀N.(N≤LENGTH U⊃U⊗IDENT1(LENGTH U-N,N)=NTHCDR(U,LENGTH U-N))⊃
; (N'≤LENGTH U⊃
; NTH(U,LENGTH U-N').U⊗IDENT1((LENGTH U-N')',N)=NTHCDR(U,LENGTH U-N')))⊃
;(∀N.N≤LENGTH U⊃U⊗IDENT1(LENGTH U-N,N)=NTHCDR(U,LENGTH U-N))
;labels: MINUSFACT11
24. (AXIOM |∀N M.N<M⊃M-N'<M|)
;labels: SUCC_LESSEQ_LESSEQ
10. (AXIOM |∀M N.M'≤N⊃M≤N|)
;labels: LESS_LESSEQSUCC
13. (AXIOM |∀M N.M<N=M'≤N|)
;labels: MINUSFACT10
23. (AXIOM |∀N M.N<M⊃M-N=(M-N')'|)
;id main ***try again***
;second part first
(proof id_main)
(assume |n<m⊃nthcdr(ident(m),n)=ident1(n,m-n)|)
(label id_main1)
(assume |n'<m|)
(label id_main2)
(derive |nthcdr(ident(m),n)=ident1(n,m-n)|
(id_main1 id_main2 succ_less_less))
;deps: (ID_MAIN1 ID_MAIN2)
;labels: MINUSFACT10
;∀N M.N<M⊃M-N=(M-N')'
;labels: SUCC_LESS_LESS
;∀M N.M'<N⊃M<N
(rw * (use minusfact10 mode: exact) (open ident1)
(use id_main2 succ_less_less mode: exact))
;NTHCDR(IDENT(M),N)=N.IDENT1(N',M-N')
;deps: (ID_MAIN1 ID_MAIN2)
;labels: CDR_NTHCDR
;∀U N.CDR NTHCDR(U,N)=NTHCDR(U,N')
(trw |nthcdr(ident m,n')|
(use cdr_nthcdr mode: exact direction: reverse)
(use * mode: exact))
;NTHCDR(IDENT(M),N')=IDENT1(N',M-N')
(ci id_main2)
;N'<M⊃NTHCDR(IDENT(M),N')=IDENT1(N',M-N')
(ci id_main1)
;(N<M⊃NTHCDR(IDENT(M),N)=IDENT1(N,M-N))⊃
;(N'<M⊃NTHCDR(IDENT(M),N')=IDENT1(N',M-N'))
(ue (a |λn.n<m⊃nthcdr(ident(m),n)=ident1(n,m-n)|)
proof_by_induction
(part 1#1 (open minus ident)) *)
;∀N.N<M⊃NTHCDR(IDENT(M),N)=IDENT1(N,M-N)
(rw * (use minusfact10 mode: exact))
;∀N.N<M⊃NTHCDR(IDENT(M),N)=IDENT1(N,(M-N')')
;labels: CAR_NTHCDR
;∀U N.N<LENGTH U⊃CAR NTHCDR(U,N)=NTH(U,N)
(ue ((u.|ident m|)(n.n)) car_nthcdr (use * mode: always))
;N<M⊃N=NTH(IDENT(M),N)
;a more compact version of the proof id main
(assume |nthcdr(ident(m),n)=n.ident1(n',m-n')|)
(trw |cdr nthcdr(ident(m),n)| (use * mode: exact))
;CDR NTHCDR(IDENT(M),N)=IDENT1(N',M-N')
(ci -2)
;NTHCDR(IDENT(M),N)=N.IDENT1(N',M-N')⊃
;CDR NTHCDR(IDENT(M),N)=IDENT1(N',M-N')
(ue (a |λn.n<m⊃nthcdr(ident(m),n)=ident1(n,m-n)|) proof_by_induction
(open ident1)
(part 1#2#1#1 (use minusfact10 succ_less_less mode: exact))
(part 1#2#1 (use cdr_nthcdr mode: exact direction: reverse))
(use * succ_less_less mode: exact)
(part 1#1 (open minus ident)))
;∀N.N<M⊃NTHCDR(IDENT(M),N)=IDENT1(N,M-N)
(rw * (use minusfact10 mode: exact))
;∀N.N<M⊃NTHCDR(IDENT(M),N)=IDENT1(N,(M-N')')
;labels: CAR_NTHCDR
;∀U N.N<LENGTH U⊃CAR NTHCDR(U,N)=NTH(U,N)
(ue ((u.|ident m|)(n.n)) car_nthcdr (use * mode: always))
;N<M⊃N=NTH(IDENT(M),N)
;perm ident
(proof perm_ident)
;only ontoness requires some help
(assume |n<length ident(m)|)(label prm_id1)
(rw * (open ident))
;N<M
(label prm_id2)
(derive |NTH(IDENT(M),N)=N| (* id_main))
(derive |member(nth(ident m,n),ident m)| (nthmember prm_id1) )
(rw * (use -2 mode: exact))
;MEMBER(N,IDENT(M))
(ci prm_id1)
;N<M⊃MEMBER(N,IDENT(M))
(trw |∀n.perm(ident n)| (open perm into onto) (use id_main mode: always) *)
;∀N.PERM(IDENT(N))
(label perm_id)
;identity left
(proof identity_left)
(assume |into u|)(label il_1)
(ue ((u.u)(v.|ident(length u)|)) def_appl_condition * (open lesseq))
;DEF_APPL(IDENT(LENGTH U),U)
(label il_2)
(rw il_1 (open into))
;∀N.N<LENGTH U⊃NATNUM(NTH(U,N))∧NTH(U,N)<LENGTH U
(ue ((v.|ident(length u)|)(u.u)) nth_compose il_2 *
(use id_main ue: ((n.|nth(u,n)|)(m.|length u|)) ))
;∀N.N<LENGTH U⊃NTH(IDENT(LENGTH U)⊗U,N)=NTH(U,N)
(ue ((u.|ident(length u)⊗u|)(v.u)) extensionality
(sortcomp il_2 length_compose *) (open appl))
;IDENT(LENGTH U)⊗U=U
(ci il_1)
;INTO(U)⊃IDENT(LENGTH U)⊗U=U
;inv main ***try again***
(proof inverse_main)
(assume |perm u|)
(label inv_main1)
(rw inv_main1 (open perm onto))
;INTO(U)∧(∀N.N<LENGTH U⊃MEMBER(N,U))
(label inv_main2)
(ue ((u.u)(y.n)) posfacts)
;(NULL FSTPOSITION(U,N)⊃¬MEMBER(N,U))∧(MEMBER(N,U)⊃NATNUM(FSTPOSITION(U,N)))
(derive |n<length u⊃¬null fstposition(u,n)| (inv_main2 *))
(label inv_main3)
(assume |n<length u⊃nthcdr(inverse(u),n)=invers1(u,n,length u-n)|)
(label inv_main5)
(assume |n'<length u|)
(label inv_main6)
(show proof_by_induction)
;labels: PROOF_BY_INDUCTION
1. (AXIOM |∀A.A(0)∧(∀N.A(N)⊃A(N'))⊃(∀N.A(N))|)
(derive |n<length u| (* succ_less_less))
(label inv_main7)
(derive |¬null fstposition(u,n)| (inv_main3 inv_main7))
(label inv_main9)
(rw inv_main5
(use inv_main7 inv_main9)(open invers1)
(use minusfact10 mode: always))
(label inv_main10)
;NTHCDR(INVERSE(U),N)=FSTPOSITION(U,N).INVERS1(U,N',LENGTH U-N')
;deps: (INV_MAIN1 INV_MAIN5 INV_MAIN6)
;labels: CDR_NTHCDR
;∀U N.CDR NTHCDR(U,N)=NTHCDR(U,N')
(ue ((u.|inverse u|)(n.n)) cdr_nthcdr (use * mode: exact))
;INVERS1(U,N',LENGTH U-N')=NTHCDR(INVERSE(U),N')
;deps: (INV_MAIN1 INV_MAIN5 INV_MAIN6)
(ci inv_main6)
;N'<LENGTH U⊃INVERS1(U,N',LENGTH U-N')=NTHCDR(INVERSE(U),N')
(ci inv_main5)
(ue (a |λn.n<length u⊃nthcdr(inverse(u),n)=invers1(u,n,length u-n)|)
proof_by_induction (part 1#1(open inverse minus)) *)
;∀N.N<LENGTH U⊃NTHCDR(INVERSE(U),N)=INVERS1(U,N,LENGTH U-N)
;deps: (INV_MAIN1)
;now the main lemma
(rw * (use minusfact10 mode: exact) (open invers1)
(use inv_main3 mode: always))
;∀N.N<LENGTH U⊃
;NTHCDR(INVERSE(U),N)=FSTPOSITION(U,N).INVERS1(U,N',LENGTH U-N')
;deps: (INV_MAIN1)
;labels: CAR_NTHCDR
;∀U N.N<LENGTH U⊃CAR NTHCDR(U,N)=NTH(U,N)
(ue ((u.|inverse(u)|)(n.n)) car_nthcdr
(use * lengthinverse inv_main1 mode: always))
;N<LENGTH U⊃FSTPOSITION(U,N)=NTH(INVERSE(U),N)
;deps: (INV_MAIN1)
(ci inv_main1)
;PERM(U)⊃(N<LENGTH U⊃FSTPOSITION(U,N)=NTH(INVERSE(U),N))
(derive |∀u n.perm u∧n<length u⊃nth(inverse u,n)=fstposition(u,n)| *)
;a more compact version of the proof inv main
(proof inverse_main)
(assume |perm u|)
(label inv_main1)
(rw inv_main1 (open perm onto))
;INTO(U)∧(∀N.N<LENGTH U⊃MEMBER(N,U))
(label inv_main2)
(ue ((u.u)(y.n)) posfacts)
;(NULL FSTPOSITION(U,N)⊃¬MEMBER(N,U))∧(MEMBER(N,U)⊃NATNUM(FSTPOSITION(U,N)))
(derive |n<length u⊃¬null fstposition(u,n)| (inv_main2 *))
(label inv_main3)
(assume |nthcdr(inverse(u),n)=fstposition(u,n).invers1(u,n',length u-n')|)
(trw |cdr nthcdr(inverse(u),n)| (use * mode: exact))
;CDR NTHCDR(INVERSE(U),N)=INVERS1(U,N',LENGTH U-N')
(ci -2)
;NTHCDR(INVERSE(U),N)=FSTPOSITION(U,N).INVERS1(U,N',LENGTH U-N')⊃
;CDR NTHCDR(INVERSE(U),N)=INVERS1(U,N',LENGTH U-N')
(ue (a |λn.n<length u⊃nthcdr(inverse(u),n)=invers1(u,n,length u-n)|)
proof_by_induction (open invers1)
(part 1#2#1#1 (use minusfact10 succ_less_less mode: exact))
(part 1#2#1 (use cdr_nthcdr mode: exact direction: reverse)
(use inv_main3 mode: exact))
(use * succ_less_less mode: exact)
(part 1#1(open inverse minus)))
;∀N.N<LENGTH U⊃NTHCDR(INVERSE(U),N)=INVERS1(U,N,LENGTH U-N)
;deps: (INV_MAIN1)
(rw * (use minusfact10 mode: exact) (open invers1)
(use inv_main3 mode: always))
;∀N.N<LENGTH U⊃
;NTHCDR(INVERSE(U),N)=FSTPOSITION(U,N).INVERS1(U,N',LENGTH U-N')
;deps: (INV_MAIN1)
;labels: CAR_NTHCDR
;∀U N.N<LENGTH U⊃CAR NTHCDR(U,N)=NTH(U,N)
(ue ((u.|inverse(u)|)(n.n)) car_nthcdr
(use * lengthinverse inv_main1 mode: always))
;N<LENGTH U⊃FSTPOSITION(U,N)=NTH(INVERSE(U),N)
;deps: (INV_MAIN1)
(ci inv_main1)
;PERM(U)⊃(N<LENGTH U⊃FSTPOSITION(U,N)=NTH(INVERSE(U),N))
;perm inverse: part 1 (into inverse)
(proof inverse_perm)
(assume |perm(u)|)(label inv_p1)
(rw * (open perm onto))(label inv_p2)
;INTO(U)∧(∀N.N<LENGTH U⊃MEMBER(N,U))
(ue ((u.u)(y.n)) posfacts)
;(NULL FSTPOSITION(U,N)⊃¬MEMBER(N,U))∧(MEMBER(N,U)⊃NATNUM(FSTPOSITION(U,N)))
(derive |∀n.n<length u⊃natnum fstposition(u,n)∧fstposition(u,n)<length u|
(inv_p2 * pos_length))
(label inv_p3)
(derive |∀n.n<length u⊃nth(inverse u,n)=fstposition(u,n)| (inv_main inv_p1))
(label inv_p4)
(rw inv_p3 (use * mode: always direction: reverse))
;∀N.N<LENGTH U⊃NATNUM(NTH(INVERSE(U),N))∧NTH(INVERSE(U),N)<LENGTH U
(trw |into inverse(u)| * (open into) (use lengthinverse inv_p1 mode: exact))
;INTO(INVERSE(U))
(label into_inverse)
(ci inv_p1)
;PERM(U)⊃INTO(INVERSE(U))
(label inv_into)
;perm inverse: part 2 (onto inverse)
;under the same assumption
;(assume |perm u|)(label inv_p1)
(rw inv_p1 (open perm into onto) )
;(∀N.N<LENGTH U⊃NATNUM(NTH(U,N))∧NTH(U,N)<LENGTH U)∧(∀N.N<LENGTH U⊃MEMBER(N,U))
(label inv_p10)
(derive |length inverse(u)=length u| (inv_p1 lengthinverse))
(label inv_p11)
(assume |n<length inverse(u)|)(label inv_p12)
(rw * (use inv_p11 mode: exact))
;N<LENGTH U
(label inv_p13)
;so we can apply the main property of the inverse function...
(ue (n |nth(u,n)|) inv_p4 (use inv_p10 * mode: always))
;NTH(INVERSE(U),NTH(U,N))=FSTPOSITION(U,NTH(U,N))
(label inv_p14)
;...a consequence of the pigeon hole principle...
(derive |inj u| (inv_p1 perm_injectivity))
(derive |fstposition(u,nth(u,n))=n|
(fstposition_nth uniqueness_injectivity * inv_p10 inv_p13))
(rw inv_p14 (use *))
;NTH(INVERSE(U),NTH(U,N))=N
(label inv_p15)
;..and the lemma nthmember
(derive |NATNUM NTH(U,N)∧NTH(U,N)<LENGTH INVERSE(U)| (inv_p10 inv_p11 inv_p13))
(trw |member(nth(inverse u,nth(u,n)),inverse u)| (nthmember *))
;MEMBER(NTH(INVERSE(U),NTH(U,N)),INVERSE(U))
;...to conclude
(rw * (use inv_p15))
;MEMBER(N,INVERSE(U))
;deps: (INV_P1 INV_P12)
(ci inv_p12)
;N<LENGTH (INVERSE(U))⊃MEMBER(N,INVERSE(U))
(label onto_inverse)
(trw |perm(inverse u)| (open perm onto) into_inverse onto_inverse)
;PERM(INVERSE(U))
(ci INV_P1)
;PERM(U)⊃PERM(INVERSE(U))
;compose_inverse_right;
(proof compose_inverse_right)
(assume |perm u|)(label cir1)
(rw cir1 (open perm onto))
;INTO(U)∧(∀N.N<LENGTH U⊃MEMBER(N,U))
(label cir2)
(derive |length inverse(u)=length u| (cir1 lengthinverse))
(label cir3)
(derive |perm inverse(u)|(perm_inverse cir1))
(rw * (open perm onto))
;INTO(INVERSE(U))∧(∀N.N<LENGTH (INVERSE(U))⊃MEMBER(N,INVERSE(U)))
(ue ((v.u)(u.|inverse u|)) def_appl_condition (cir3 *) (open lesseq))
;DEF_APPL(U,INVERSE(U))
(label cir4)
(trw |length(u⊗inverse(u))=length ident(length u)|
(use length_compose ue: ((w.u)(u.|inverse u|)) cir4 mode: always)
(use cir3))
;LENGTH (U⊗INVERSE(U))=LENGTH (IDENT(LENGTH U))
(label cir5)
;so we can apply nth_compose...
(ue ((v.u)(u.|inverse u|)) nth_compose cir4 cir3)
;∀N.N<LENGTH U⊃NTH(U⊗INVERSE(U),N)=NTH(U,NTH(INVERSE(U),N))
;...inv_main...
(rw * (use inv_main cir1 mode: always))
;∀N.N<LENGTH U⊃NTH(U⊗INVERSE(U),N)=NTH(U,FSTPOSITION(U,N))
;...nth_fstposition...
(rw * (use nth_fstposition cir2 mode: always))
;∀N.N<LENGTH U⊃NTH(U⊗INVERSE(U),N)=N
;...to conclude, using id_main
(trw |∀n.n<length u⊃nth(u⊗inverse(u),n)=nth(ident(length u),n)|
(use * mode: always)(use id_main ue: ((m.|length u|)(n.n)) mode: always))
;∀N.N<LENGTH U⊃NTH(U⊗INVERSE(U),N)=NTH(IDENT(LENGTH U),N)
(label cir6)
(ue ((u.|u⊗inverse(u)|)(v.|ident(length u)|)) extensionality cir6
(use cir5 mode: always)(use sortcomp cir4 mode: always))
;U⊗INVERSE(U)=IDENT(LENGTH U)
(ci CIR1)
;PERM(U)⊃U⊗INVERSE(U)=IDENT(LENGTH U)
;labels: EXTENSIONALITY
;(AXIOM |∀U V.LENGTH U=LENGTH V∧(∀I.I<LENGTH U⊃APPL(U,I)=APPL(V,I))⊃U=V|)
;labels: LENGTH_COMPOSE
;(AXIOM |∀W U.DEF_APPL(W,U)⊃LENGTH (W⊗U)=LENGTH U|)
;labels: NTH_FSTPOSITION
;(AXIOM |∀U N.MEMBER(N,U)⊃NTH(U,FSTPOSITION(U,N))=N|)
;labels: INV_MAIN
;(AXIOM |∀U N.PERM(U)∧N<LENGTH U⊃NTH(INVERSE(U),N)=FSTPOSITION(U,N)|)
;labels: ID_MAIN
;(AXIOM |∀M N.N<M⊃NTH(IDENT(M),N)=N|)
;labels: NTH_COMPOSE
;(AXIOM |∀V U N.DEF_APPL(V,U)∧N<LENGTH U⊃NTH(V⊗U,N)=NTH(V,NTH(U,N))|)
;labels: DEF_APPL_CONDITION
;(AXIOM |∀U V.INTO(U)∧LENGTH U≤LENGTH V⊃DEF_APPL(V,U)|)
;compose inverse left; ***try again***
;want
;labels: compose_inverse_left
;∀U.PERM(U)⊃INVERSE U⊗U=IDENT(LENGTH U)
(proof compose_inverse_left)
(assume |perm u|)(label cil1)
(derive |length inverse(u)=length u| (lengthinverse *))
(label cil2)
(rw cil1 (open perm onto))
;INTO(U)∧(∀N.N<LENGTH U⊃MEMBER(N,U))
(label cil3)
(ue ((v.|inverse u|)(u.u)) def_appl_condition cil2 cil3 (open lesseq)
(use perm_inverse cil1))
;DEF_APPL(INVERSE(U),U)
(label cil4)
(trw |listp inverse(u)⊗u| (cil4 sortcomp))
;LISTP INVERSE(U)⊗U
(label cilsort)
(derive |length(inverse(u)⊗u)=length ident(length u)| (cil4 length_compose))
(label cil5)
(assume |n<length u|)(label cil6)
;use the lemma nth_inverse...
(ue ((v.|inverse u|)(u.u)(n.n)) nth_compose cil4 cil6)
;NTH(INVERSE(U)⊗U,N)=NTH(INVERSE(U),NTH(U,N))
(label cil7)
;...the main property of inverse...
(rw cil3 (open into))
;(∀N.N<LENGTH U⊃NATNUM(NTH(U,N))∧NTH(U,N)<LENGTH U)∧(∀N.N<LENGTH U⊃MEMBER(N,U))
(label cil8)
(ue ((u.u)(n.|nth(u,n)|)) inv_main (use cil1 cil6 cil8 mode: always))
;NTH(INVERSE(U),NTH(U,N))=FSTPOSITION(U,NTH(U,N))
(label cil9)
;...a consequence of the pigeon_hole principle...
(derive |inj u| (perm_injectivity cil1))
(label cil10)
;...the lemma fstposition_nth...
(derive |fstposition(u,nth(u,n))=n|
(fstposition_nth uniqueness_injectivity cil10 cil6))
(rw cil9 (use *))
;NTH(INVERSE(U),NTH(U,N))=N
;and the main property of ident to conclude:
(trw |nth(inverse(u)⊗u,n)=nth(ident(length u),n)| (use cil6 cil7 * mode: always)
(use id_main ue: ((m.|length u|)(n.n)) cil6 mode: always))
;NTH(INVERSE(U)⊗U,N)=NTH(IDENT(LENGTH U),N)
(ci cil6)
;N<LENGTH U⊃NTH(INVERSE(U)⊗U,N)=NTH(IDENT(LENGTH U),N)
;therefore
(ue ((u.|inverse(u)⊗u|)(v.|ident(length u)|)) extensionality
cil5 * cilsort (open appl))
16. ;INVERSE(U)⊗U=IDENT(LENGTH U)
;deps: (CIL1)
(ci cil1)
;PERM(U)⊃INVERSE(U)⊗U=IDENT(LENGTH U)
;;;;;;;;;
;labels: EXTENSIONALITY
;∀U V.LENGTH U=LENGTH V∧(∀I.I<LENGTH U⊃APPL(U,I)=APPL(V,I))⊃U=V
;labels: DEF_APPL_CONDITION
;∀U V.INTO(U)∧LENGTH U≤LENGTH V⊃DEF_APPL(V,U)
;labels: NTH_COMPOSE
;∀V U N.DEF_APPL(V,U)∧N<LENGTH U⊃NTH(V⊗U,N)=NTH(V,NTH(U,N))
;labels: INV_MAIN
;∀U N.PERM(U)∧N<LENGTH U⊃NTH(INVERSE(U),N)=FSTPOSITION(U,N)
;labels: FSTPOSITION_NTH
;∀U N.UNIQUENESS(U)∧N<LENGTH U⊃FSTPOSITION(U,NTH(U,N))=N
;labels: ID_MAIN
;∀M N.N<M⊃NTH(IDENT(M),N)=N
;labels: LENGTH_COMPOSE
;∀W U.DEF_APPL(W,U)⊃LENGTH (W⊗U)=LENGTH U
;labels: LENGTH_COMPOSE
;∀W U.DEF_APPL(W,U)⊃LENGTH (W⊗U)=LENGTH U